Nuprl Lemma : es-realizer_wf 11,40

P:(ES{i}{i'}), p:es-real{i:l}(es.P(es)). es-realizer(p es_realizer{i:l} 
latex


Definitionsxt(x), t.1, es-realizer(p), t  T, x(s), , x:AB(x), x:AB(x), es.P(es)
Lemmasevent system wf, es-real wf

origin